
%%% Thesis Introduction --------------------------------------------------

\chapter{Введение}

\ifpdf
    \graphicspath{{Introduction/IntroductionFigs/PNG/}{Introduction/IntroductionFigs/PDF/}{Introduction/IntroductionFigs/}}
\else
    \graphicspath{{Introduction/IntroductionFigs/EPS/}{Introduction/IntroductionFigs/}}
\fi


\def\baselinestretch{1.5}


\section{Введение в  $\lambda$ - исчисление} % section headings are printed smaller than chapter names
\subsection{Предварительные сведения}
В $\lambda$ - исчислении две операции: применение и абстракция. 
\begin{description}
  \item[Применение (Application)]: Означает применение или вызов функции по отношению 
к заданному значению. Её обычно обозначают F X, где F - функция,а X - значение.
С точки зрения программиста: F трактуется как алгоритм, вычисляющий результат 
по заданному входному значению,т.е. F (алгоритм) применяется к X (входные данные). 
Так же возможно самоприменение, те F F. 
  \item[Абстракция (Abstraction)]: Пусть M = M[x] — выражение, содержащее x. Тогда 
$\lambda$ x. M обозначает функцию x $\to$ M[x], то есть каждому x сопоставляется M[x].
Если x в M[x] отсутствует, то $\lambda$x.M — константная функция со значением M. 
\end{description}
Применение и абстракция работают совместно: \\
\textbf{Пример:} 
Т.к. выражение $\lambda$x. 2 $\times$ x + 1 обозначает функцию, ставящую в соответсвие каждому 
x значение 2 $\times$ x + 1, то для вычисления выражения ($\lambda$x. 2 $\times$ x + 1) 42 необходимо: 
\begin{center}
($\lambda$x. 2 $\times$ x + 1) 42 = 2 $\times$ 42 + 1 = 85. 
\end{center}

То есть ($\lambda$x. 2 $\times$ x + 1) 42 - применение функции x \to 2 $\times$ x + 1 к аргументу 42, 
дающее в результате 2 $\times$ 42 + 1. \\
\hspace*{\fill} 
\subsection{Термы}
\textbf{Опр}. Множество $\lambda$-термов $\Lambda$ строится из переменных \\ V = \{x, y, z, ...\} с помощью 
применения и абстракции: \\
\begin{center}
x $\in$ V $\Rightarrow$ x $\in$ $\Lambda$\\
M, N $\in$ $\Lambda$ $\Rightarrow$ (MN) $\in$ $\Lambda$ \\
M $\in$ $\Lambda$, x $\in$ V $\Rightarrow$ ($\lambda$x.M) $\in$ $\Lambda$ \\
\end{center} 
Более удобно для написания использовать следующий абстрактный синтаксис: \\
\begin{center}
$\Lambda$ ::= V | ($\Lambda$$\Lambda$) | ($\lambda$V.$\Lambda$)
\end{center} 

Введем несколько соглашений:
\begin{itemize}
  \item Внешние скобки опускаются
  \item Применение ассоциативно влево: 
\begin{center}
FXYZ обозначает (((FX)Y)Z) 
\end{center} 
  \item Абстракция ассоциативна вправо:  
\begin{center}
$\lambda$xyz.M обозначает ($\lambda$x($\lambda$y($\lambda$z.(M)))) 
\end{center} 
\end{itemize}
\subsection{Свободные и связанные переменные}
Прежде, чем рассматривать преобразования выражений, введем важное понятие свободной и связанной переменной. \\
Неформально говоря, вхождение переменной в некоторое выражение будет связанным, если оно находится внутри
некоторого лямбда-выражения, в заголовке которого эта переменная упомянута в качестве аргумента. 
Если переменная не является связанной в некотором выражении, то она в нем будет свободной. \\

Определим понятия свободных и связанных переменных более формально. \\

\textbf{Опр.} Абстракция $\lambda$x.M[x] связывает дотоле свободную переменную x в терме M. \\

\textbf{Примеры:} 
\begin{center}
($\lambda$y. ($\lambda$x.xz)y)w
\end{center} 

Переменные x и y - связанные, а z и w - свободные.\\
Следует отметить, что одна и та же переменная может быть связанной в некотором выражении и одновременно свободной в некотором его подвыражении. 

\begin{center}
($\lambda${\color{red}x}. ($\lambda${\color{green}x}.{\color{green}x}z){\color{green}x}){\color{blue}x}
\end{center} 

Переменная x - связанная(дважды) и свободная, а z - свободная. \\
\textbf{Опр.} Множество FV(T) свободных переменных в $\lambda$-терме T определяется индуктивно: \\

\begin{center}
FV(x) = \{x\} \\
FV(MN) = FV(M) $\cup$ FV(N) \\
FV($\lambda$x.M) = FV(M) $\setminus$ \{x\} \\
\end{center} \hspace*{\fill} 

\textbf{Опр.} Множество BV(T) связанных переменных:

\begin{center}
BV(x) = $\varnothing$ \\
BV(MN) = BV(M) $\cup$ BV(N) \\
BV($\lambda$x.M) = BV(M) $\cup$ \{x\} \\
\end{center} \hspace*{\fill} 

\textbf{Опр.} M - замкнутый $\lambda$-терм(или комбинатор), если FV(M) = $\varnothing$. Множество замкнутых $\lambda$-термов 
обозначается через $\Lambda^{0}$. \\
\subsection{Понятие $\beta$ - редукции}
{\color{blue}Поставим вопрос: как доказать неравенство термов?} \hspace*{\fill} \\
Рассмотрим примеры: \\
\begin{itemize}
\item KI $\equiv$ ($\lambda$xy.x) ($\lambda$z.z) = ($\lambda$yz.z) 
\item IIK_{*} $\equiv$ ($\lambda$x.x)IK_{*} = IK_{*} $\equiv$ ($\lambda$yz.z) 
\end{itemize} 
Очевидно, что процесс носит односторонний характер: термы при конверсиях "упрощаются". Для исследования 
подобного вычислительного аспекта вводят понятие редукции: 
\begin{itemize}
\item KI $\to_{\beta}$ $K_{*}$ - редуцируется за один шаг 
\item $IIK_{*}$ $\twoheadrightarrow_{\beta}$ $K_{*}$ - редуцируется 
\item KI $=_{\beta}$ $IIK_{*}$ - конвертируемо(равно)
\end{itemize} 
Если в некоторое выражение входит в качестве подвыражения такое выражение, к которому можно применить одну из редукций, то такое подвыражение называется редуцируемым или сокращенно редексом. \\

\textbf{Опр.} Терм типа ($\lambda$x.M)N называется $\beta$-редексом. \\
\textbf{Опр.} Бинарное отношение R над $\Lambda$ называют совместимым (с операциями $\lambda$-исчисления), если \\

\begin{center}
M R N => (Z M) R (Z N) \\
M R N => (MZ) R (N Z), \\
M R N => ($\lambda$x .M) R ($\lambda$x . N).  \\
\end{center} 

\textbf{Опр.} Совместимое отношение эквивалентности называют отношением конгруэнтности над $\Lambda$. \\
\textbf{Опр.} Совместимое, рефлексивное и транзитивное отношение называют отношением редукции над $\Lambda$.\\

\\
Неформально говоря, преобразование, называемое $\beta$-редукцией, соответствует применению функции, представленной $\lambda$-выражением, к аргументу. Если исходное выражение имело вид ($\lambda$x.e) a, то в результате применения $\beta$-редукции оно будет преобразовано в e{x|a} - выражение e, в котором все свободные вхождения переменной x заменены на выражение a. \\

Дадим формальное определение:\\

\textbf{Опр.} Бинарное отношение $\beta$-редукции за один шаг $\to_{\beta}$ $\Lambda$ над :\\

\begin{center}
($\lambda$x.M) N $\to_{\beta}$  M[x := N] \\
M $\to_{\beta}$ N \Rightarrow Z M $\to_{\beta}$ Z N \\
M $\to_{\beta}$ N \Rightarrow M Z $\to_{\beta}$ N Z \\
M $\to_{\beta}$ N \Rightarrow $\lambda$x.M $\to_{\beta}$ $\lambda$x.N \\
\end{center}  

\textbf{Пример}:\\
($\lambda$yz.y)($\lambda$p.p) $\to_{\beta}$ $\lambda$zp.p \\ 

\textbf{Опр.} Бинарное отношение $\beta$-редукции многошаговой $\twoheadrightarrow_{\beta}$ над $\Lambda$ определяется индуктивно:\\

\begin{center}
M $\twoheadrightarrow_{\beta}$ M \\
M $\twoheadrightarrow_{\beta}$ N \Rightarrow M $\twoheadrightarrow_{\beta}$ N \\
M $\twoheadrightarrow_{\beta}$ N, N $\twoheadrightarrow_{\beta}$ L \Rightarrow M $\twoheadrightarrow_{\beta}$ L \\
\end{center} 

\textbf{Пример}: \\
($\lambda$x.x)(($\lambda$yz.y)($\lambda$p.p)) $\twoheadrightarrow_{\beta}$ $\lambda$zp.p \\

Отношение $\twoheadrightarrow_{\beta}$ является транзитивным рефлексивным замыканием $\to_{\beta}$ и, следовательно, отношением редукции. \\
Заметим, что при применении $\beta$-редукции замене подлежат именно свободные переменные тела лямбда-выражения. \\

\section{Просто типизированное $\lambda$-исчисление}

В этом разделе будет введена система $\lambda$$\to$ просто типизированного лямбда-исчисления. 
\subsection{Типы}
Типы обычно представляют собой объекты синтаксической природы и могут быть присвоены лямбда термам. \\
Если M - такой терм и тип $\sigma$ присвоен M, то будем говорить "M имеет тип $\sigma$", используемая при этом нотация имеет вид M : $\sigma$.

Можно сравнить типы, присвоенные термам, с размерностями физических величин, хотя такую аналогию нельзя назвать совершенной. Подобные физические размерности защищают нас от неправильных операций вроде сложения двух вольт и трех ампер.\\

Похожим образом типы, присвоенные $\lambda$-термам, обеспечивают частичную спецификацию алгоритмов, которые те предоставляют, и полезны для демонстрации их частичной корректности. Типы могут быть также использованы для увеличения эффективности компиляции термов, предоставляющих функциональные алгоритмы. \\

\textbf{Опр.} Стрелочный тип: \\
В большинстве систем типизации тождественной функции I $\equiv$ $\lambda$x.x может быть приписан тип $\alpha$ $\to$ $\alpha$ 

\begin{center}
I:$\alpha$ $\to$ $\alpha$
\end{center} 

Если x, являющийся аргументом функции I, имеет тип $\alpha$, то значение Ix тоже имеет тип $\alpha$. \\
В общем случае $\alpha$ $\to$ $\beta$ является типом функции из $\alpha$ в $\beta$.
\subsection{Системы в стиле Карри и Черча}
Две основополагающие статьи Карри и Черча, вводящих типизированные варианты $\lambda$-исчисления, порождают два различных семейства система. \\

В типизированном $\lambda$-исчислении в стиле Карри термы являются теми же самыми, что и в бестипотовой теории. Каждый терм обладает множеством различных типов. Это множество может быть пустым, состоять из одного элемента, или из некоторого числа элементов(возможно и бесконечного). \\

В системах типа Чёрча термы представляют собой аннотированные версии бестиповых термов. Каждый терм имеет тип, который обычно уникален(с точностью до отношения эквивалентности) и который может быть выведен из способа, которым терм аннотирован.\\

Подходы Карри и Черча к типизации $\lambda$-исчисления соответствуют двум парадигмам в программировании. В рамках первой из них программы могут записываться безо всякого использования типов. В этом случае возможность присвоения типа программе должен проверить компилятор. Это произойдет, если программа правельна. Хорошо известным примером такого языка может служить ML. Такой стиль типизации называют неявной типизацией (например, Haskell, Ocaml).\\

Противоположная парадигма в программировании носит название явной типизации; она соответствует версии Черча типизированного лямбда-исчисления. При

этом программа должна быть записана вместе со своим типом. Проверка типов для таких языков обычно оказывается более простой, поскольку отсутствует необходимость конструировать типы.Примером таких языков могут служить ALGOL68. Некоторые авторы называют карриевские системы “$\lambda$-исчислением с присваиванием типов”, а черчевские системы — “системами типизированного $\lambda$-исчисления”.\\

Замечание: Далее мы будем рассматривать ТОЛЬКО системы типа Карри\\

\subsection{Просто типизированное $\lambda$ исчисление}
\textbf{Опр.} Самая простая система — это просто типизированное $\lambda$ исчисление( $\lambda$$\to$, нотация Type($\lambda$$\to$)) определена ниже индуктивно. Будем писать T = Type($\lambda$$\to$).

\begin{center}
Переменные типа : $\alpha$, $\beta$ ... $\in$ T \\
Типы пространства функций : $\delta$, $\tau$ $\in$ T => ($\delta$ $\to$ $\tau$) $\in$ T \\
\end{center}

Более удобно для написания T использовать следующий абстрактный синтаксис: \\

T ::= V | T$\to$ T	\\

Введем несколько базисных определений: \\
\textbf{Опр.} 
\begin{description}
  \item[Высказывание]: имеет вид M:$\sigma$, где M $\in$$\Lambda$ и $\sigma$$\in$T. Тип $\sigma$ является предикатом, а терм M-субъектом высказывания.
  \item[Объявление]: это высказывание с переменной(термовой) в качестве субъекта. 
  \item[Базис]: это множество объявлений с различными переменными в качестве субъекта.
\end{description}

\hspace*{\fill} \\
\textbf{Опр.} Высказывание M:$\sigma$ называется выводимым из базиса Г, обозначение 

\begin{center}
Г $\vdash$ M:$\sigma$
\end{center}

,если вывод Г $\vdash$ M:$\sigma$ может быть произведен по следующим правилам

\begin{center}
(x:$\sigma$)$\in$Г $\Rightarrow$ Г $\vdash$ M:$\sigma$ (аксиома)\\
Г $\vdash$ M:($\sigma$$\to$$\tau$), Г $\vdash$ N:$\sigma$ $\Rightarrow$ Г $\vdash$ (MN):$\tau$ (удаление $\to$)\\
Г, x:$\sigma$ $\vdash$ M:$\tau$ $\Rightarrow$ Г $\vdash$ ($\lambda$x.M):$\sigma$$\to$$\tau$ (введение $\to$)\\
\end{center}

\textbf{Пример 1}: x: $\alpha$, y: $\alpha$ \to $\beta$. Тогда (xy):$\beta$\\

\textbf{Пример 2}: Пусть x: $\alpha$ тогда ($\lambda$x. x) : $\alpha$ \to $\alpha$.\\



\section{Алгоритм вывода типов}

\subsection{Унификатор}

Для осуществления унификации необходимо понятие подстановки типов. \\

Подстановкой типов называется отображение S из множества типов в него же, такое что вместо заданного типа $\tau$ подставляется некоторый другой тип $\sigma$. Базовые типы могут подставляться только сами в себя, а вместо типовой переменной можно подставить любой другой тип, который не включает в себя эту типовую переменную. Подстановка для стрелки осуществляется по схеме: 

\begin{center}

S($\sigma$ $\to$ $\tau$) $\equiv$ S($\sigma$)$\to$S($\tau$)

\end{center} 

Обычно подстановка тождественна на всех типовых переменных, кроме конечного носителя sup(S) = \{$\alpha$|S($\alpha$) $\not$$\equiv$ $\alpha$\} \\
Если S($\sigma$) = $\tau$, то тип $\tau$ называется примером типа $\sigma$.

\textbf{Опр.} Композиция подстановок - подстановка с носителем, являющимся объединением носителей. Для \\

\begin{center}

S = [$\alpha$:=$\gamma$$\to$$\beta$,$\beta$:=$\alpha$$\to$$\gamma$] \\
T = [$\alpha$:=$\beta$$\to$$\gamma$,$\gamma$:=$\beta$]

\end{center} 

имеем

\begin{center}

S$\circ$T = [$\alpha$:=T(S($\alpha$)), $\beta$:=T(S($\beta$)), $\gamma$:=T(S($\gamma$))] 

\end{center} 

то есть

\begin{center}

S$\circ$T = [$\alpha$:=$\beta$$\to$$\beta$, $\beta$:=($\beta$$\to$$\gamma$)$\to$$\beta$, $\gamma$:=$\beta$] 

\end{center} 

Замечание: подстановки - моноид относительно $\circ$ с единицей []. \\

\textbf{Опр.} Унификатор для типов $\delta$ и $\tau$ — это подстановка S, такая что S($\delta$) = S($\tau$). \\

\textbf{Опр.} Унификатор S — это главный унификатор для $\delta$ и $\tau$, если для любого другого унификатора $S^{\prime}$ существует подстановка T, такая что $S^{\prime}$ = T $\circ$ S \\

Унификация производится на паре типов. Также необходимо отметить, что операция унификации некоммутативна. Этот процесс односторонен — результат приведения первого типа ко второму в общем случае не равен результату приведения второго типа к первому. Пример: константу невозможно унифицировать переменной, а переменная унифицируется константой, принимая в качестве конкретного значения её саму. \\

\subsection{Теорема унификации}

\textbf{Теорема унификации.} \\

Существует алгоритм унификации U, который для заданных типов $\delta$ и $\tau$ возвращает: \\
\begin{enumerate}
\item Главный унификатор S для $\delta$ и $\tau$, если $\delta$ и $\tau$ могут быть унифицированы; \\
\item Сообщение об ошибке в противном случае.\\
\end{enumerate}
\\

Алгоритм U($\delta$, $\tau$) позволяет искать "минимальное" решение уравнения на типы $\delta$ $~$ $\tau$

\subsection{Унификация системы уравнений на типы}

Если система уравнений E=\{ $\delta$ $\equivalent$ $\tau$, ... , $\delta$ $\equivalent$ $\tau$\}, то ей унификатором называют такую подстановку S, что 
\begin{center}
S($\delta$) $\equiv$ S($\tau$) $\cap$ ... $\cap$ S($\delta$) $\equiv$ S($\tau$)
\end{center} 

Главный унификатор для системы E ищется с помощью алгоритма U следующим образом:

\begin{center}
U(E) = U($\delta_{1}$ $\to$ ... $\to$$\delta_{n}$, $\tau_{1}$$\to$ ... $\to$$\tau_{n}$)
\end{center} 

\subsection{Понятие наиболее общего типа(Главного типа)}
Для начала введем определение нумералов Черча и действий над ними.\\
\textbf{Опр.} Числа(нумералы) Черча в виде $\lambda$-термов выглядят следующим образом: \\
\begin{center}
0 = $\lambda$s z. z \\

1 = $\lambda$ s z. s z \\

2 = $\lambda$ s z. s (s z) \\

3 = $\lambda$ s z. s (s (s z)) \\

4 = $\lambda$ s z. s (s (s (s z)))\\

 ... \\
\end{center}
Каждый нумерал Черча является итератором, который соответствующее число раз применяет функцию s к результату предыдущего применения этой функции. \\

Более формальная запись нумералов Черча: \\

Выражение F^{n}(X), где n $\in$N, F, X $\in$ $\Lambda$, определим индуктивно: \\

\begin{center}

F^{0}(X) $\equiv$ X\\
F^{n+1}(X) $\equiv$ F(F^{n}(X))\\

\end{center} 

Тогда n-ое число Черча будет определяться как:\\

\begin{center}

n $\equiv$ $\lambda$sz.s^{n}(z)\\

\end{center} 

В качестве базовых операций над нумералами Черча вводятся функции для сложения, умножения и возведения в степень.(Для более углубленного рассмотрения данного материала можно порекомендовать [1] и [5])

\begin{enumerate}       % Add notes to yourself that will be displayed when
\item ADD = $\lambda$mnfx.mf(nfx) – сложение
\item MLT = $\lambda$mnf.m(nf) – умножение 
\item EXP = $\lambda$mn.nm – возведение в степень
\end{enumerate}       % Add notes to yourself that will be displayed when



Рассмотрим нулевой нумерал Черча $\lambda$s z. z \\
$${z: \alpha \;\;\;\; z:\beta}\over{0:\alpha \to \beta \to \beta}$$ \\
Но с другой стороны \\
$${z: \alpha \;\;\;\; z:\alpha}\over{0:\alpha \to \alpha \to \alpha}$$ 
\hspace*{\fill} \\

Однако, первый «лучше» в том смысле, что второй получается из него подстановкой типа вместо типовой переменной. Поэтому первый называется наиболее общим типом. \\

Введем формально определения главного типа и пары. \\

\textbf{Опр.} Для M $\in$ $\Lambda$ главной парой называют пару (Г, $\sigma$), такую что \\
\begin{enumerate}
\item Г $\vdash$ M:$\sigma$ 
\item Г' $\vdash$ M:$\sigma^{\prime}$ $\Rightarrow$ $\exist$ S [S(Г) Г' $\cap$ S($\sigma$) $\equiv$ $\sigma^{\prime}$]
\end{enumerate}
\\

\textbf{Опр.} Для M $\in$ $\Lambda^{0}$ главным типом(наиболее общим типом) называют тип $\sigma$, такой что \\
\begin{enumerate}
\item $\vdash$ M:$\sigma$ 
\item $\vdash$ M:$\sigma^{\prime}$ $\Rightarrow$ $\exist$ S [S($\sigma$) $\equiv$ $\sigma^{\prime}$] 
\end{enumerate}

Общим последнее определение, таким образом наиболее общим типом называется такой тип заданного выражения, к которому можно привести любой другой тип, который может быть приписан этому выражению. \\



Если (Г, $\sigma$) = PP(M), то FV(M) = dom(Г)\\ 

\subsection{Теорема Хинди-Миллера}

Суть системы типизации Хинди — Миллера заключается в том, что на уровне синтаксиса программы можно провести формальные преобразования таким образом, чтобы автоматически определить типы выражений, используемых в этой программе. Это избавляет разрабочика от необходимости явно указывать типы выражений, что в свою очередь влечёт за собой лаконичность и высокую степень читаемости кода программ. \\

\textbf{Теорема Хинди-Миллера.} \\

Существует алгоритм PP, возвращающий для M $\in$$\Lambda$\\
\begin{enumerate}
\item Главную пару (Г, $\sigma$), если M имеет тип \\
\item сообщение об ошибке в противном случае \\
\end{enumerate}

Алгоритм автоматического вывода типов строит систему уравнений, неизвестными в которой являются типы, после чего решает эту систему, находя неизвестные значения. Базовый вариант алгоритма достаточно прост, поэтому он неоднократно переоткрывался независимо друг от друга различными исследователями в области информатики и прикладной математики. \\

Алгоритм PP можно задать так \\

\begin{center}

PP(M) | U(E(Г^{0}, M, $\sigma^{0}$)) = ошибка = ошибка \\
PP(M) | U(E(Г^{0}, M, $\sigma^{0}$)) = S = (S(Г^{0}), S($\sigma^{0}$)) \\

\end{center} 

\section{System F}

\subsection{$\lambda$-куб}

\textbf{Опр.} Лямбда-куб ($\lambda$-куб) задает единообразное описание восьми различных систем типизированного лямбда-исчисления с явным приписыванием типов (систем, типизированных по Чёрчу).\\

\begin{figure}[h]

\centering

\includegraphics[width=7cm, height=6cm]{lambda-cube.png} 

\caption{Лямбда-куб.} 

\label{fig.0} 

\end{figure} 

\textbf{Замечание}: стрелка вдоль каждого ребра указывает на отношение включения. \\

Система $\lambda$$\to$ представляет собой просто типизированное $\lambda$-исчисление, оно было определено в разделе 1.2. Система $\lambda$2 - это полиморфное типизированное $\lambda$-исчисление.

\subsection{System F}

В $\lambda$$\to$ невозможно повторное использование: 

\begin{center}

($\lambda$$x^{\alpha}$. x) : $\alpha$ $\to$ $\alpha$ \\
($\lambda$$x^{\beta}$. x) : $\beta$ $\to$ $\beta$ \\
($\lambda$$x^{\gamma\to\sigma}$. x) : ($\gamma$$\to$$\sigma$) $\to$ $\gamma$$\to$$\sigma$ \\

\end{center} 

- три разные функции. \\

Даже в версии Карри, типизируя терм 

\begin{center}

($\lambda$y. y)($\lambda$x. x)\\

\end{center} 

имеем x:$\sigma$, y:$\sigma$$\to$$\sigma$, ($\lambda$x. x):$\sigma$$\to$$\sigma$, ($\lambda$y. y):($\sigma$$\to$$\sigma$)$\to$$\sigma$$\to$$\sigma$ \\

В результате делая одну экспансию получим нетипизируемое:\\

\begin{center}

($\lambda$f. ff)($\lambda$x. x)\\

\end{center} 

Идея: добавить нотацию полиморфизма к определению просто типизированного $\lambda$-исчисления

\begin{center}

($\lambda$x. x) : $\forall$ $\alpha$.  $\alpha$ $\to$ $\alpha$ \\

($\lambda$x y. x) : $\forall$ $\alpha$.$\forall$ $\beta$. $\alpha$ $\to$ $\beta$ $\to$ $\alpha$ \\

\end{center} 

Теперь вместо типовой переменной под квантором всеобщности можно подставить любой тип: 

\begin{center}

($\alpha$ $\to$ $\alpha$) [$\alpha$ := $\gamma$] $\Rightarrow$ ($\lambda$x. x) : $\gamma$ $\to$ $\gamma$ \\

($\alpha$ $\to$ $\alpha$) [$\alpha$ := $\gamma$ $\to$ $\gamma$] $\Rightarrow$ ($\lambda$x. x) : ($\gamma$ $\to$ $\gamma$) $\to$ $\gamma$ $\to$ $\gamma$ \\

($\alpha$ $\to$ $\alpha$) [$\alpha$ := $\gamma$ $\to$ $\beta$ $\to$ $\gamma$] $\Rightarrow$ ($\lambda$x. x) : ($\gamma$ $\to$ $\beta$ $\to$ $\gamma$) $\to$ $\gamma$ $\to$ $\beta$ $\to$ $\gamma$ \\

\end{center} 

Более удобно для написания использовать следующий абстрактный синтаксис: \\

T ::= V | T$\to$ T| $\forall$VT	\\

Это определяет \textbf{$\lambda$2} — лямбда-исчисление второго порядка или System F \\ 

% There you go. You already know the most important things.





% ----------------------------------------------------------------------


